(set-option :print-success false)
(set-option :produce-interpolants true)
(set-logic QF_LIA)
(declare-fun x_1 () Int)
(declare-fun xm1 () Int)
(declare-fun x2 () Int)
(declare-fun res4 () Int)
(declare-fun resm5 () Int)
(declare-fun xm6 () Int)
(declare-fun x7 () Int)
(declare-fun res9 () Int)
(declare-fun resm10 () Int)
(declare-fun res11 () Int)
(assert (! (<= x_1 100) :named M1))
(assert (! (= xm1 (+ x_1 11)) :named M2))
(assert (! (> x2 100) :named S11))
(assert (! (= res4 (- x2 10)) :named S12))
(assert (! (and (= x2 xm1) (= resm5 res4)) :named S1RET))
(assert (! (= xm6 resm5) :named M3))
(assert (! (> x7 100) :named S21))
(assert (! (= res9 (- x7 10)) :named S22))
(assert (! (and (= x7 xm6) (= resm10 res9)) :named S2RET))
(assert (! (= res11 resm10) :named M4))
(assert (! (and (<= x_1 101) (distinct res11 91)) :named ERR))
(check-sat)
;unsat
(get-interpolants M1 M2 (and S11 S12) S1RET M3 (and S21 S22) S2RET M4 ERR)
;((<= x_1 100)
; (<= xm1 111)
; true
; (<= res4 (- x2 10))
; (<= resm5 101)
; (<= xm6 101)
; (>= x7 101)
; (and (>= res9 91) (<= res9 (- x7 10)))
; (= resm10 91)
; (= res11 91))
